\begin{tabbing}
$e$:$s$.$P$($s$)@$j$ 
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. vartype($j$;$x$) $\subseteq$r ${\it ds}$($x$)?Top)\+
\\[0ex]c$\wedge$ \=($\forall$${\it e'}$@$j$. (${\it e'}$ $<$ $e$) $\Rightarrow$ ($P$(state after ${\it e'}$) $\vee$ ($\exists$${\it e''}$:E. ((${\it e'}$ $<$loc ${\it e''}$) \& (${\it e'}$ $<$ $e$))))\+
\\[0ex]\& $\forall$${\it e'}$@$j$. ($e$ $<$ ${\it e'}$) $\Rightarrow$ ($P$((state when ${\it e'}$)) $\vee$ ($\exists$${\it e''}$:E. ((${\it e''}$ $<$loc ${\it e'}$) \& ($e$ $<$ ${\it e'}$)))))
\-\-
\end{tabbing}